We recall here the general notations together with some elements of  the semantics of high-level Petri nets \cite{DBLP:series/eatcs/Jensen92}.
\begin{definition}[high-level Petri nets]\label{def:PTS}
A \emph{high-level Petri net} $N$ is a tuple $(Q, T,  F, L, M_0)$ where:
\begin{itemize}
 \item $Q$ is the set of places,

 \item $T$ is the set of transitions and $Q \cap T = \emptyset$;

 \item $F \subseteq (Q \times T) \cup (T \times Q)$ is the set of arcs; 
 \item $L$ is the labeling function from places $Q$, transitions $T$ and arcs $F$   to  a set of labels defined as follows:
\renewcommand{\labelitemii}{$-$} 
\begin{itemize}
 \item $\forall q \in Q$, $L(q) $ is the type of $q$, \ie a (possibly infinite) set or Cartesian product of sets of integer values;
 \item $\forall t \in T$, $L(t)$ is a  computable boolean expression  with variables and integer values; 
 \item and $\forall f\in F$, $L(f)$  is a  tuple of variables and integer values compatible with the adjacent place.  
\end{itemize}
 \item $M_0$ is the initial marking which associates to each place  $q \in Q$ a multiset of tokens in $L(q)$.
\end{itemize} 
\end{definition}

Observe that we are considering a subclass of high-level Petri nets where at most one arc per direction  for each pair place/transition   is allowed and only one token can flow through. 
We denote the set of input places of a transition $t$ by $\pre{t} =\{q\in Q \mid (q,t) \in F\}$. % and analogously the set of output places of $t$ by $\post{t} =\{q\in Q \mid (t,q) \in F\}$. 
The behavior of high-level Petri nets is defined as usual: markings are functions from places in $Q$ to multisets of tokens $L(q)$ and  a transition $t \in T$ is \emph{enabled} at  marking $M$, if there exists an evaluation $\sigma$ of all variables in the labeling of $t$ and of its adjacent  input and  output arcs such that: 
$$L_{\sigma}(t) = \mathsf{true}  \qquad \text{ and } \qquad \forall q \in \pre{t},   L_{\sigma}((q,t)) \in M(q).$$
then, the firing of $t$ produces the marking $M'$,  denoted $\firing{M}{t}{\sigma}{M'}$:  
$$\forall q \in Q, M'(q) = M(q) - L_{\sigma}((q,t)) + L_{\sigma}((t,q)). $$
with $L_{\sigma}(f) = 0 $ if $f\notin F$, $-$ and $ +$ are  multiset  operators for removal and adding of one element, respectively.%  into a multiset.

By convention, primed version of variables (e.g. $x'$) are used to annotate  output arcs of transitions, their evaluation is  possibly computed using unprimed variables (e.g. $x$ and $y$) appearing on input arcs. With an abuse of notation, singleton markings are denoted without brackets, the same is used in  arc annotations. An example of firing is shown in  Figure \ref{fig:exfiring}. 
We say that a marking $M$ is \emph{reachable} from the initial marking $M_0$ if there exists a firing sequence $(t_1, \sigma_1), \dots, (t_n, \sigma_n)$ such that 
 $\firing{M_0}{t_1}{\sigma_1}{M_1} \dots \firing{M_{n-1}}{t_n}{\sigma_n}{M}$.



 \begin{figure}[t]
\centering
\subfigure[Before the firing\label{fig:before}]{
\begin{tikzpicture}[node distance=1.5cm,>=stealth',bend angle=45,auto]

 \tikzstyle{place}=[circle,thick,draw=blue!75,fill=blue!30,minimum size=7mm]
 \tikzstyle{transition}=[rectangle,thick,draw=black!75,
 			 fill=black!20,minimum size=4mm]
 \tikzstyle{every token}=[font=\small]

  \node [place, label = left: $q_1$] at (0,1.5) (Q1){$7$};
  \node [place, label=left:$q_2$]at (0,-1.5)  (Q2){$5$};
  \node [place, label = right: $q_3$] at (1.5,0) (Q3){};
  
  \node [transition] (t) [  label={[red] left:$\begin{array}{lc}
                                                &x>y \\ L(t)=&\wedge \\ &x'=x+y
                                               \end{array}$}] at (0,0) {$t$}
   edge [pre]    node[right] {$x$}    (Q1)
   edge [pre]    node[right] {$y$}    (Q2)
   edge [post]   node[above]{$x'$}    (Q3);
\end{tikzpicture}} \quad
\subfigure[After the firing \label{fig:after}]{
\begin{tikzpicture}[node distance=1.5cm,>=stealth',bend angle=45,auto]

 \tikzstyle{place}=[circle,thick,draw=blue!75,fill=blue!30,minimum size=7mm]
 \tikzstyle{transition}=[rectangle,thick,draw=black!75,
 			 fill=black!20,minimum size=4mm]
 \tikzstyle{every token}=[font=\small]

  \node [place, label = left: $q_1$] at (0,1.5) (Q1){};
  \node [place, label=left:$q_2$]at (0,-1.5)  (Q2){};
  \node [place, label = right: $q_3$] at (1.5,0) (Q3){12};
  
  \node [transition] (t) [  label={[red] left:$\begin{array}{lc}
                                                &x>y \\ L(t)=&\wedge \\ &x'=x+y
                                               \end{array}$}] at (0,0) {$t$}
   edge [pre]    node[right] {$x$}    (Q1)
   edge [pre]    node[right] {$y$}    (Q2)
   edge [post]   node[above]{$x'$}    (Q3);
\end{tikzpicture}}
\caption{Example of firing with $\sigma = \{ x= 7, y=5, x'=12\}$.} \label{fig:exfiring}
\end{figure}
 